We introduce a new semantics for a logic of explicit and implicit beliefs based on the concept of multi-agent belief base. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and doxastic/epistemic alternative are primitive, in our semantics they are non-primitive but are defined from the concept of belief base. We provide a complete axiomatization and prove decidability for our logic via a finite model argument. We also provide a polynomial embedding of our logic into Fagin & Halpern's logic of general awareness and establish a complexity result for our logic via the embedding.

Logics of knowledge based on possible-world semantics are u seful in many areas of knowledge representation and reasoning, ranging from security t o distributed computing to game theory. In these models, an agent is said to know a fact ϕ if ϕ is true in all the worlds she considers possible. While reasoning about knowledge with t his semantics has proved useful, as is well known, it suffers from what is known in the literature as the logical omniscience problem: under possible-world semantics, agents know all t autologies and know the logical consequences of their knowledge. While logical omniscience is certainly not always an issue, in many applications it is. For example, in the context of distributed computing, we are interested in polynomial-time algorithms, although in some cases the knowledge needed to p erform optimally may require calculations that cannot be performed in polynomial time (u nless P=NP) [Moses and Tuttle 1988]; in the context of security, we may want to reason about computationally bounded adversaries who cannot factor a large composite number, and thus cannot be logically omniscient; in game theory, we may be interested in the impac t of computational resources on solution concepts (for example, what will agents do if com puting a Nash equilibrium is difficult). Not surprisingly, many approaches for dealing with the logi cal omniscience problem have been suggested (see [Fagin, Halpern, Moses, and Vardi 1 995, Chapter 9] and [Moreno 1998]).

Awareness has been shown to be a useful addition to standard epistemic logic for many applications. However, standard propositional logics for knowledge and awareness cannot express the fact that an agent knows that there are facts of which he is unaware without there being an explicit fact that the agent knows he is unaware of. We propose a logic for reasoning about knowledge of unawareness, by extending Fagin and Halpern's \emph{Logic of General Awareness}. The logic allows quantification over variables, so that there is a formula in the language that can express the fact that ``an agent explicitly knows that there exists a fact of which he is unaware''. Moreover, that formula can be true without the agent explicitly knowing that he is unaware of any particular formula. We provide a sound and complete axiomatization of the logic, using standard axioms from the literature to capture the quantification operator. Finally, we show that the validity problem for the logic is recursively enumerable, but not decidable.